M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). M.ef(k,x,s,v)?w  M.ds(x) 

latex

Definitions	MsgA, M.state, M.da(a), M.ds(x), M.ef(k,x,s,v)?w, IdDeq, KindDeq, Unit, P  Q, P & Q, P  Q, x  dom(f), product-deq(A;B;a;b), a:A fp B(a), 1of(t), x. t(x), , Prop, b, A, b, x:A. B(x), Top, f(x), f(x)?z, 2of(t), Valtype(da;k), State(ds), Id, Knd, t  T
Lemmas	assert wf, not wf, bnot wf, bool wf, pi2 wf, fpf-cap wf, pi1 wf, ma-valtype wf, fpf-trivial-subtype-top, product-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, Knd wf, ma-state wf, top wf, Kind-deq wf, Id wf, id-deq wf, msga wf, fpf-ap wf, subtype rel self